Nuprl Lemma : Rall-cons
0,22
postcript
pdf
u
,
v
,
R
:Top.
x
u
.
v
.
R
(
x
) ~ (
R
(
u
)
x
v
.
R
(
x
))
latex
Definitions
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
(
L
)
,
x
L
.
R
(
x
)
Lemmas
top
wf
origin
u, v, R:Top. 
x
u.v.R(x) ~ (R(u) xv.R(x)) u, v, R:Top. xu.v.R(x) ~ (R(u) xv.R(x)) Tx:A. B(x)(L)xL.R(x)